\begin{tabbing}
msg{-}spec{-}loc{-}decl(${\it snd}$;$i$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$k$:Knd, $l$:IdLnk.\+
\\[0ex]fpf{-}dom(product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq); $\langle$$k$$,\,$$l$$\rangle$; ${\it snd}$)
\\[0ex]$\Rightarrow$ \=source($l$) $=$ $i$ $\in$ Id\+
\\[0ex]\& l\_all(map\=($\lambda$$p$.1of($p$)\+
\\[0ex];fpf{-}ap(\=${\it snd}$; product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq); $\langle$$k$$,\,$$l$$\rangle$\+
\\[0ex]));Id;${\it tg}$.fpf{-}dom(KindDeq; rcv($l$,${\it tg}$); ${\it da}$))
\-\-\-\-
\end{tabbing}